Nuprl Lemma : can-apply-compose'
11,40
postcript
pdf
A
,
B
,
C
:Type,
g
:(
A
(
B
+ Top)),
f
:(
A
B
C
),
x
:
A
. can-apply(
f
o'
g
;
x
) ~ can-apply(
g
;
x
)
latex
ProofTree
Definitions
left
+
right
,
s
=
t
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
Top
,
Type
,
f
(
a
)
,
P
Q
,
do-apply(
f
;
x
)
,
can-apply(
f
;
x
)
,
f
o'
g
,
s
~
t
Lemmas
top
wf
origin
A, B, C:Type, g:(A
(B + Top)), f:(ABC), x:A. can-apply(f o' g;x) ~ can-apply(g;x)
A, B, C:Type, g:(A(B + Top)), f:(ABC), x:A. can-apply(f o' g;x) ~ can-apply(g;x)
TB(x)x:A. B(x)
Q